home *** CD-ROM | disk | FTP | other *** search
/ PC-Blue - MS DOS Public Domain Library / PC-Blue MS-DOS Public Domain Library - NYACC.iso / vol350 / prolog.arc / LOGIC.ARC / LOXED.PRO next >
Encoding:
Text File  |  1987-04-03  |  10.9 KB  |  283 lines
  1. /*
  2.  Note from Bob: To run this on types FS and higher, you have to
  3. substitute another symbol for "&", or use "hidedef". Also, the
  4. "inttoasc" clause I have included should be replaced by "atoi"
  5. for efficiency. Also note that "members" is a "built-in" in types
  6. FS and higher, so the definition should be deleted.
  7. */
  8.  
  9.           /* program LOXED.PRO, propositional logic tutorial, 
  10.           author Xavier Salazar Resines,
  11.             27th january  1987         */
  12.  
  13. ?-hidelog; true.
  14. ?-op(200,xfy,'<=>').
  15. ?-op(190,xfy,'=>').
  16. ?-op(180,xfy,'v').
  17. ?-op(170,xfy,'&').
  18. ?-op(160,fy,'~').
  19.  
  20.  
  21. disp_menu :- menu ; true.
  22.  
  23. menu:- cls,
  24. nl,print('                        M E N U'),
  25. nl,nl,print('          i = instructions,'),
  26. nl,nl,print('          o = operators,'),nl,
  27. nl,print('          e = erase argument,'),nl,
  28. nl,print('          a = introduce an argument and test it(end each with `.`),'),
  29. nl,
  30. nl,print('          l = list or test with rules (at end write menu? <RET>),'),
  31. nl,nl,print('          s: exit the program,'),nl,
  32. nl,print('          EXIT the system: s + ^C + s <RET>.'),nl,nl,
  33. print('                                       Choice (^P) '), ratom(X), X.
  34.  
  35. i:- ins,ratom(_),menu.
  36. o:- ops,ratom(_),menu.
  37. e:- erase,menu.
  38. a:- prem,ratom(_),menu.
  39. l:- ord.
  40. s.
  41.  
  42. /* entering premises & conclusion, build list for WANG test */
  43. prem:- cls,print('!! To begin a new process, first: erase'), nl,
  44.        print('Erased (y/n)? '), ratom(S),S = 'y',cls,
  45.        print('SYSTEM: L O X'),nl,print('Number of premises: '),
  46.        rnum(Np),retract(np(Q)),asserta(np(Np)),nl,print('P r e m i s e s :'),
  47.        nl,print('-----------------'),nl,expres(Np,T).
  48. prem.
  49.  
  50. expres(Np,T):- Np =< 0, print('\t','|- '),retract(ergo(X)),read(Erg),
  51.          asserta(ergo(Erg)),theorem(T => Erg),!, fail.
  52. expres(Np,T):- 
  53.     num(N),Q is N+1,Q = 1,!, retract(num(N)), asserta(num(Q)),
  54.     makename(Den,[r,Q]), print(Den),print(' '), read(Ter), Z is Np - 1, 
  55.     asserta(r(Den(Ter))),expres(Z,Ter).
  56. expres(Np,T):-
  57.     Np > 0, num(N), Q is N+1,retract(num(N)), asserta(num(Q)),
  58.     makename(Den,[r,Q]),print(Den),print(' '),read(Ter),Z is Np - 1, 
  59.     asserta(r(Den(Ter))),expres(Z,T & Ter).
  60.  
  61. /* initialize r)ow, j)ustification, ergo (conclusion), num(ber, np (number of
  62.    premises, rf (reference number) */
  63. r(nein).
  64. j(nein).
  65. ergo(nein).
  66. num(0).
  67. np(0).
  68. rf(0).
  69.  
  70. /* print process */
  71. ord:- cls,rf(X), premises(X).
  72. ord:- conclusion.
  73. ord:- np(X),proof(X).
  74.  
  75. premises(X):- np(R),Z is X + 1, Z =< R,  makename(Den,[r,Z]), r(Den(M)),
  76.        print(Den(M)),curwh(X,62),print('(P)'),nl,
  77.        premises(Z).
  78.  
  79. conclusion:- ergo(C),np(R), Z is R + 1,print('\t',' |- '),write(C),
  80.              curwh(R,60),print('(conclusion) ').
  81.  
  82. proof(X):- num(Lim), Z is X + 1,Z =< Lim, makename(Den,[r,Z]),r(Den(M)),
  83.            makename(Jus,[j,Z]),j(Jus(N)),curwh(Z,1),print(Den(M)),
  84.            curwh(Z,62),print(N),nl,proof(Z).
  85. proof(X):- makename(Den,[r,X]),r(Den(M)),Z is X + 1, finis(Z,M).
  86.  
  87. /* erase an argument */
  88. erase:- retract(r(M)),retract(j(N)),retract(num(P)),asserta(num(0)),
  89.      retract(ergo(Q)), asserta(r(nein)),asserta(j(nein)),
  90.      asserta(ergo(nein)). 
  91.  
  92. /* modus ponens */
  93. mp(R1, R2) :- r(R1((X => Y))), r(R2(X)),num(Q),Z is Q + 1,
  94.     retract(num(Q)),asserta(num(Z)),makename(Den,[r,Z]),asserta(r(Den(Y))),
  95.     makename(Jus,[j,Z]),asserta(j(Jus([mp,R1,R2]))),ord.
  96.  
  97. /* addition */
  98. ad(R1, W):- r(R1(Y)),num(Q),Z is Q + 1,
  99.      retract(num(Q)),asserta(num(Z)),makename(Den,[r,Z]),asserta(r(Den((Y v W)))),
  100.      makename(Jus,[j,Z]),asserta(j(Jus([ad,R1]))),ord.
  101.  
  102. /* conjunction */
  103. cj(R1,R2):-r(R1(X)),r(R2(Y)),num(Q),Z is Q + 1,
  104.       retract(num(Q)),asserta(num(Z)),makename(Den,[r,Z]),asserta(r(Den((X & Y)))),
  105.       makename(Jus,[j,Z]),asserta(j(Jus([cj,R1,R2]))),ord.
  106.  
  107. /* simplification */
  108. sp(R1):- r(R1((X & Y))), num(Q),Z is Q + 1,retract(num(Q)),asserta(num(Z)),
  109.          makename(Den,[r,Z]),asserta(r(Den(X))),makename(Jus,[j,Z]),
  110.      asserta(j(Jus([sp,R1]))),ord.
  111.  
  112. /* commutativity */
  113. cm(R1):- r(R1((X & Y))),num(Q),Z is Q + 1,retract(num(Q)),asserta(num(Z)),
  114.     makename(Den,[r,Z]),asserta(r(Den((Y & X)))),makename(Jus,[j,Z]),
  115.     asserta(j(Jus([cm,R1]))),ord.
  116. cm(R1):- r(R1((X v Y))),num(Q),Z is Q + 1,retract(num(Q)),asserta(num(Z)),
  117.     makename(Den,[r,Z]),asserta(r(Den((Y v X)))),makename(Jus,[j,Z]),
  118.     asserta(j(Jus([cm,R1]))),ord.
  119.  
  120. tr(R1,R2):- r(R1((X => Y))),r(R2((Y => W))),num(Q),Z is Q + 1,retract(num(Q)),
  121.      asserta(num(Z)),makename(Den,[r,Z]),asserta(r(Den((X => W)))),makename(Jus,[j,Z]),
  122.      asserta(j(Jus([tr,R1,R2]))),ord.
  123.  
  124. /* de Morgan law */
  125. dm(R1):- r(R1(~(X & Y))),num(Q),Z is Q + 1,retract(num(Q)),asserta(num(Z)),
  126.        makename(Den,[r,Z]),asserta(r(Den((~X v ~Y)))),
  127.        makename(Jus,[j,Z]),asserta(j(Jus([dm,R1]))),ord.
  128. dm(R1):- r(R1(~(X v Y))),num(Q),Z is Q + 1,retract(num(Q)),asserta(num(Z)),
  129.        makename(Den,[r,Z]),asserta(r(Den((~X & ~Y)))),
  130.        makename(Jus,[j,Z]),asserta(j(Jus([dm,R1]))),ord.
  131.  
  132. /* transform => to v, or viceversa, by definition */
  133. df(R1):- r(R1((X => Y))),num(Q),Z is Q + 1,retract(num(Q)),asserta(num(Z)),
  134.        makename(Den,[r,Z]),asserta(r(Den((~X v Y)))),makename(Jus,[j,Z]),
  135.        asserta(j(Jus([df,R1]))),ord.
  136. df(R1):- r(R1((X v Y))),num(Q),Z is Q + 1,retract(num(Q)),asserta(num(Z)),
  137.        makename(Den,[r,Z]),asserta(r(Den((~X => Y)))),makename(Jus,[j,Z]),
  138.        asserta(j(Jus([df,R1]))),ord.
  139.  
  140. /* contraposition */
  141. ct(R1):- r(R1((X => Y))),num(Q),Z is Q + 1,retract(num(Q)),asserta(num(Z)),
  142.        makename(Den,[r,Z]),asserta(r(Den((~Y => ~X)))),makename(Jus,[j,Z]),
  143.        asserta(j(Jus([ct,R1]))),ord.
  144.  
  145. /* double negation in a term */
  146. nodn(~ ~ H,H):- !.
  147. nodn(L,L).
  148.  
  149. /* double negation */
  150. dn(R1):- r(R1((X & Y))),nodn(X,Nx),nodn(Y,Ny),num(Q),Z is Q+1,makename(Den,[r,Z]),
  151.         retract(num(Q)),asserta(num(Z)),makename(Jus,[j,Z]),
  152.         asserta(j(Jus([dn,R1]))),asserta(r(Den((Nx & Ny)))),ord.
  153. dn(R1) :- r(R1((X => Y))),nodn(X,Nx),nodn(Y,Ny),num(Q),Z is Q+1,
  154.       makename(Den,[r,Z]),retract(num(Q)),asserta(num(Z)),makename(Jus,[j,Z]),
  155.       asserta(j(Jus([dn,R1]))),asserta(r(Den((Nx => Ny)))),ord.
  156. dn(R1):- r(R1((X v Y))),nodn(X,Nx),nodn(Y,Ny),num(Q),Z is Q+1,makename(Den,[r,Z]),
  157.         retract(num(Q)),asserta(num(Z)),makename(Jus,[j,Z]),
  158.         asserta(j(Jus([dn,R1]))),asserta(r(Den((Nx v Ny)))),ord.
  159. dn(R1):- r(R1((X <=> Y))),nodn(X,Nx),nodn(Y,Ny),
  160.     num(Q),Z is Q+1,makename(Den,[r,Z]),retract(num(Q)),asserta(num(Z)),
  161.     makename(Jus,[j,Z]),asserta(j(Jus([dn,R1]))),asserta(r(Den((Nx <=> Ny)))),
  162.     ord.
  163.  
  164. /* double negation in a single term */
  165. dns(R1):- r(R1((X))),nodn(X,Nx),num(Q),Z is Q+1,
  166.     makename(Den,[r,Z]),retract(num(Q)),asserta(num(Z)),makename(Jus,[j,Z]),
  167.     asserta(j(Jus([dns,R1]))),asserta(r(Den((Nx)))),ord.
  168.  
  169. /* verification of validity, test by rules */
  170. finis(Z,X):-ergo(Erg),X = Erg,S is Z+1,curwh(S,20),
  171.       print(' q.e.d.          SYSTEM: L O X'),!.
  172.  
  173.               /* WANG Algorithm */
  174.  
  175. theorem(T):- prove([] & [] => [] & [T]),!,nl,
  176.          print(' VALID argument   L O X').
  177. theorem(_):- nl,print('INVALID argument   L O X').
  178.  
  179. prove(E1):- rule(E1,E2),!, prove(E2).
  180.  
  181.         /* v at left. */
  182. prove(L & [H v I|T] => R):- !,
  183.         prove(L & [H|T] => R),
  184.         prove(L & [I|T] => R).
  185.  
  186.         /*  & at right. */
  187. prove(L => R & [H & I|T]):- !,
  188.         prove(L => R & [H|T]),
  189.         prove(L => R & [I|T]).
  190.  
  191.         /* atom */
  192. prove(L & [H|T] => R):- !,prove([H|L] & T => R).
  193. prove(L => R & [H|T]):- !,prove(L => [H|R] & T).
  194.  
  195.         /* Verify tautology */
  196. prove(T):- tautology(T),!.
  197. prove(_):- fail.
  198.  
  199. tautology(L & [] => R & []):- members(M,L), members(M,R).
  200.  
  201.         /*  => appears in one side */
  202. rule(L & [H => I|T] => R,
  203.     L & [~ H v I|T] => R).
  204. rule(L => R & [H => I|T],
  205.     L => R & [~ H v I|T]).
  206.  
  207.         /*  <=> appears in one side */
  208. rule(L & [H <=> I|T] => R,
  209.     L & [(H => I) & (I => H)|T] => R).
  210. rule(L => R & [H <=> I|T], L => R & [(H => I) & (I => H)|T]).
  211.  
  212.         /* appears ~ */
  213. rule(L & [~ H|T] => R & R2, L & T => R & [H|R2]).
  214. rule(L1 & L2 => R & [~ H|T], L1 & [H|L2] => R & T).
  215.  
  216.         /* & at left */
  217. rule(L & [H & I|T] => R, L & [H,I|T] => R).
  218.  
  219.         /* v at right */
  220. rule(L => R & [H v I|T], L => R & [H,I|T]).
  221.  
  222.         /* Ends WANG */
  223.  
  224. members(H,[H|_]).
  225. members(I,[_|T]):- members(I,T).
  226.  
  227. ops:- cls,print('SYSTEM: L O X'),nl,
  228. print('operators (ended with a POINT !!!):'),nl,
  229. print('implication:  (x => y).'),nl,
  230. print('conjunction:  (x & y).'),nl,
  231. print('disyunction:  (x v y).'),nl,
  232. print('equivalence:  (x <=> y).'),nl,
  233. print('negation:     ~x.'),nl,nl,
  234. print('rules:'),nl,
  235. print('mp((p => q),p)        => q          modus ponens,'),nl,
  236. print('tr((p => q),(q => r)) => (p => r)   transitivity,'),nl,
  237. print('dm(~(p & q))          => (~p v ~q)  de Morgan,'),nl,
  238. print('dm(~(p v q))          => (~p & ~q)  de Morgan,'),nl,
  239. print('df((p => q))          => (~p v q)   definition,'),nl,
  240. print('df((p v q))           => (~p => q)  definition,'),nl,
  241. print('ct((p => q))          => (~q => ~p) contraposition,'),nl,
  242. print('sp((p & q))           => p          simplification,'),nl,
  243. print('cm((p & q))           => (q & p)    commutativity,'),nl,
  244. print('cm((p v q))           => (q v p)    commutativity,'),nl,
  245. print('ad(p,h)               => (p v h)    addition (h is external),'),nl,
  246. print('cj(p,q)               => (p & q)    conjunction,'),nl,
  247. print('dn(R(X,Y))            => double negation expression 2 arguments,'),nl,
  248. print('dns(R)                => double negation ONE argument.'),nl,
  249. print('--------------------------------------------------------------------'). 
  250. ins:- cls,print('SYSTEM: L O X'),nl,print('INSTRUCTIONS'),nl,
  251.     print('-------------'),nl,
  252.       print('1. ERASE before introducing an argument,'),nl,
  253.       print('2. write the premises and after  |- write the conclusion,'),nl,
  254.       print('3. each premise or conclusion must be ended with a POINT,'),nl,
  255.     print('4. after writing the conclusion wait the automatic validity test,'),
  256.       nl,print('5. for the TEST use the connectives and operators sintax,'),
  257.       nl,print('6. for the TEST write op(r#,r##)? <RET>,'),
  258.    nl,print('7. to print the process list: shift + PrtSc,'),nl,
  259.       print('8. to print instructions or operators: ^P, at the end ^P'),
  260.    nl,print('9. to RETURN TO THE MENU press ` and <RET>.'),nl,
  261.  print('NOTES:'),nl,
  262.   print('If a double negation occurs in a complex expression, you must'),
  263.    nl,print('simplify it first. Example:'),nl,    
  264.       print('                       ((~ ~p => q) & (~ ~q v ~ ~t))'),nl,
  265.       print('must be separated in  '),nl,
  266.       print('                       (~ ~p => q)  and  (~ ~q v ~t)    '),
  267.    nl,print('Double negations must be separeted between themselves.'),
  268. nl,print('In expressions WITHOUT BINARY connectives,ex: ~ ~p, use dns(R).').
  269.     
  270.  
  271. makename( X, [Letter,Number] ) :- 
  272.         inttoasc( Number, Chars ),
  273.         name( Numname, Chars ),
  274.     concat( X, [Letter, Numname] ).
  275.  
  276. inttoasc( N, [C] ) :- N < 10, !, C is N+48.
  277. inttoasc( N, [C|Cs] ) :-
  278.     C is (N mod 10) + 48,
  279.     N1 is N/10,
  280.     inttoasc( N1, Cs ).
  281.  
  282. ?-disp_menu.
  283.